/* -*- Mode:Prolog; coding:ISO-8859-1; -*- */


:- use_module(library(clpfd)).
:- use_module(library(lists)).
:- use_module(library(terms)).
:- use_module(inequalities).
:- use_module(library(timeout)).
:- use_module(library(system)).

:- ensure_loaded([preprocessing,
                  abduction,
                  list_utils,
                  blackboard]).
                  
      
:- dynamic modename/2, originalic/1.
:- op(600, fx, '#').

:- dynamic additional_info/2.

learn(Examples, Background, Modedecs, ICs, Solution) :-
        tempfilemake(FileNameC), 
        preprocessing(Examples, Modedecs, Background, ICs, FileNameC),  log('Loading theory in the abductive engine'),
        loadandquery(FileNameC, Solution).

learn_dg(ExamplesForGoal, _Examples, Background, Modedecs, ICs, Solution) :-
        tempfilemake(FileNameC),         
        preprocessing(ExamplesForGoal, Modedecs, Background, ICs, FileNameC),  log('Loading theory in the abductive engine'),
        loadandquery(FileNameC, Solution).            


tempfilemake(FileNameC) :-
        (directory_exists('../temp/') -> true; make_directory('../temp')),
        concat_atoms('../temp/', temp, FileNameC).               
  
loadandquery(FileNameC, Solution) :-
        load_theory(FileNameC), !,                                      log('Learning starting...'),
        check_learning_preconditions,
        (querywtimeout(Solution), ! ; true).
        
querywtimeout(Solution) :-
        bb_get_value(timeout, TimeOut),
        (TimeOut == false ->
                                %0 means it will find all solutions. Actually it's just a way
                                %to ask the abductive system to find all solutions
                                %the number of solutions is checked when a new inductive solution is derived
                                        heuristics_query([goal], Solution) 
                                ;
                                        TimeOut = MS,                                           print('Executing with timeout '), log(MS),
                                        time_out(heuristics_query([goal], Solution), MS, Result),
                                        (Result = time_out ->
                                                                                                log('Timeout occurred'),
                                                findall(RTTX, (retractme(RTTX), erase(RTTX)), _)
                                        ;
                                                true
                                        )
       ).                



check_learning_preconditions :-
        (bb_get_value(ic_check, true) ->
                (predicate_property(ic, _) -> true; log('ERROR: There must me at least one ic declared (or disable ic_check mod)'), halt)
                ;
                true).





preprocessing(E, M, B, IC, FileName) :-
        init_learning_top(E, M), %At the end of this, what goes in the abductive file is asserted
        findall(Clause, for_the_top(Clause), TOP),
        retractall(for_the_top(_)),
        produce_file_for_abduction(TOP, B, IC, M, FileName).


%@     @item   produce_file_for_abduction(+TOP, +B, +IC,  ?FileName).
%@                Given all the needed inputs for the ILP task, it creates a file that can be used
%@                by an abductive system whose path is in FileName.
%@                If FileName is not given, it is by default 'temp'
produce_file_for_abduction(TOP, B, IC, M, FileName) :-
        (var(FileName) -> FileName = 'temp'; true),
        (file_exists(FileName) -> delete_file(FileName); true),
      %  make_b_for_ic(B, TOP, B2),
        make_ic_for_ic(IC, M, IC2),
        append([IC2, B, TOP], FinalList),        
        list_to_file(FinalList, FileName).


init_learning_top(E, M) :-
        make_top_theory(M),
        add_abducible_heads,
        reverse(E,ER),
        make_examples(ER, MetaExamples),
        reverse(MetaExamples, XM),
        make_goal(XM),
        make_statics.



%Everything that goes in the top theory is asserted and retrieved afterwards (for lighter predicates)
:- dynamic for_the_top/1.

%@    @item    make_top_theory(+M, -TOP)
%@    Given Mode declarations M, returns the top theory TOP.
make_top_theory(M) :-
        findall(
                HeadModeDec, 
                (member(HeadModeDec, M), functor(HeadModeDec, modeh, _)), 
                ListOfModeh
        ), 
        findall(
                BodyModeDec, 
                (member(BodyModeDec, M), functor(BodyModeDec, modeb, _)), 
                ListOfModeb
        ), 
        make_head_clauses(ListOfModeh),               
        make_body_clauses(ListOfModeb).
        
        

%@ @item make_head_clauses(+ListOfModeh).
%@ ListOfModeh is a list of head mode declarations of different arity of the type modeh(..., ..., ...).
%@ TopHeads is the list of clauses that are built.
%@ Builds a head grammar clause for each element of ListOfModeh.
make_head_clauses(ListOfModeh) :- 
        make_head_clauses(ListOfModeh, 1).

make_head_clauses([], _).
make_head_clauses([H | TListOfModeh], N) :- 
        make_head_clause(H, N), 
        NN is N + 1, 
        make_head_clauses(TListOfModeh, NN).



%@ @item make_body_clauses(+ListOfModeb).
%@ ListOfModeb is a list of head mode declarations of different arity of the type modeb(..., ..., ...).
%@ TopBodies is the list of clauses that are built.
%@ Builds a head grammar clause for each element of ListOfModeb.
make_body_clauses(ListOfModeb) :- 
        make_body_clauses(ListOfModeb, 1).



make_body_clauses([], _).
make_body_clauses([H | TListOfModeb], N) :- 
        make_body_clause(H, N), 
        NN is N + 1, 
        make_body_clauses(TListOfModeb, NN).








%@ @item make_head_clause(+HeadDec, -ClauseId).
%@ Given a mode declaration it produces a clause for the top theory.
make_head_clause(HeadDec, ClauseId) :- 
        functor(HeadDec, modeh, Arity),
        arg(1, HeadDec, SchemaOrRecall),
         (number(SchemaOrRecall) ->
                log('Recall in head not supported'),
                 (Arity > 2 ->                                   %if there is more than one argument, the second is the options
                        arg(3, HeadDec, ModeOptions);           
                        ModeOptions = [])
          ;
                Schema = SchemaOrRecall,
                arg(1, HeadDec, Schema),                 %the first argument is the schema
                (Arity > 1 ->                                   %if there is more than one argument, the second is the options
                        arg(2, HeadDec, ModeOptions);           
                        ModeOptions = [])
         ),  
         (member(name(NAME), ModeOptions) ->             %replaces the clauseId wih a name, if declared
                FinalId = NAME; 
                FinalId = ClauseId),
        assert(modename(FinalId, HeadDec)),
        dissection(Schema, AllArguments, DissectionedLiteral), 
        generate_vars_and_type_check(AllArguments, InputVars, _OutputVars, ConstantVars, AllVars, TCheckIn, TCheckC, TCheckO),
        length(InputVars, LIV),
        assert(additional_info(outputs_in(FinalId), LIV)),
        variabilise(DissectionedLiteral, AllVars, VariabilisedDissectionedLiteral), 
        make_literal(VariabilisedDissectionedLiteral, Head),!,
        /*
        At this point we have e.g. for modeh(animal(+c, t(+s, ouch(-p, #q)))
                            Head = animal(A, t(B, ouch(C, D)))
                            InputVars = [A, B]
                            OutputVars = [C]
                            ConstantVars = [D]
                            TCheckIn = [c(A), s(B)]
                            TCheckRest = [p(C), q(D)]
        */
        append(TCheckIn, TCheckC, AppendTemp1),
        append(AppendTemp1, TCheckO, TypeChecksList),
        list2conjunction(TypeChecksList, TypeChecks),
        List = 
        [       arwr(Head),        
                check_vars(AllVars),
                        make_output_list([], TCheckIn, OutputList),
                        pr(0, [(FinalId, ConstantVars, [])]),
                        gpr(0, [(FinalId, ConstantVars, [])]), 
                        make_output_list([], TCheckO, OutputVarsN),
                        body(OutputList, 1, [(FinalId, ConstantVars, [])], OutputVarsN),
                        TypeChecks
        ],
        list2conjunction(List, Body),
        C = (Head :- Body),
        assertz(for_the_top(C)).






%@ make_body_clause(+ModeB, +ClauseId).
%@         ModeB of the type modeb(habitat(+animal,#habitat), +1, [option(...)])
%@         ClauseId is an integer
%@         It returns the corresponding top theory clause Outb for the mode declaration
make_body_clause(BodyDec, ClauseId) :- 
        functor(BodyDec, modeb, Arity),
        arg(1, BodyDec, SchemaOrRecall),
        (number(SchemaOrRecall) ->
                arg(2, BodyDec, Schema),
                (Arity > 2 ->                                   %if there is more than one argument, the second is the options
                        arg(3, BodyDec, ModeOptions);           
                        ModeOptions = [])
          ;
                Schema = SchemaOrRecall,
                                 %the first argument is the schema
                (Arity > 1 ->                                   %if there is more than one argument, the second is the options
                        arg(2, BodyDec, ModeOptions);           
                        ModeOptions = [])                
        ),  
        (member(name(NAME), ModeOptions) ->             %replaces the clauseId wih a name, if declared
                        FinalId = NAME; 
                        FinalId = ClauseId),
	    (number(SchemaOrRecall) ->
        		print('Asserting recall '), print(additional_info(recall(FinalId), SchemaOrRecall)), nl,
                assert(additional_info(recall(FinalId), SchemaOrRecall))
                ;
                true
        ),
        assert(modename(FinalId, modeb(Schema, ModeOptions))),
        bb_get_value(max_body_literals, MBL),
        dissection(Schema, AllArguments, DissectionedLiteral),
        generate_vars_and_type_check(AllArguments, InputVars, OutputVars, ConstantVars, AllVars, TCheckIn, TCheckC, TCheckO),
        length(OutputVars, LOV),
        assert(additional_info(outputs_in(FinalId), LOV)),
        variabilise(DissectionedLiteral, AllVars, VariabilisedDissectionedLiteral),
        make_literal(VariabilisedDissectionedLiteral, Condition), !, 
        make_link_conditions(TCheckIn, OutputVarsFromPrevious, InputVars, LinkConditionsList, ReturnLinkList), 
        append(TCheckIn, TCheckC, AppendTemp1),
        append(AppendTemp1, TCheckO, TypeChecksList),
        list2conjunction(TypeChecksList, TypeChecks),
        list2conjunction(LinkConditionsList, LinkConditions),
        bb_get_value(score_before_condition, SBC),
        (SBC = true ->
                List =
                        [
                                Level =< MBL, 
                                append(CHyp, [(FinalId, ConstantVars, ReturnLinkList)], HHH),
                                LinkConditions,
                                verify(HHH),
                                pr(Level, HHH),
                                TypeChecks,
                                %Here the HHH is ground, except constants that are managed by CLPFD
                                verify_order(HHH),
                                gpr(Level,  HHH),
                                Condition,
                                make_output_list(OutputVarsFromPrevious, TCheckO, OutputVarsNext),
                                %append(OutputVarsFromPrevious, OutputVars, OutputVarsNext),
                                LevelN is Level + 1,
                                body(OutputVarsNext, LevelN, HHH, OutFromHead)
                        ]
        ;
                List =
                        [
                                Level =< MBL, 
                                append(CHyp, [(FinalId, ConstantVars, ReturnLinkList)], HHH),
                                LinkConditions,
                                verify(HHH),
                                pr(Level, HHH),
                                Condition,
                                TypeChecks,
                                %Here the HHH is ground, except constants that are managed by CLPFD
                                verify_order(HHH),
                                gpr(Level,  HHH),
                                make_output_list(OutputVarsFromPrevious, TCheckO, OutputVarsNext),
                                %append(OutputVarsFromPrevious, OutputVars, OutputVarsNext),
                                LevelN is Level + 1,
                                body(OutputVarsNext, LevelN, HHH, OutFromHead)
                        ]
        ),
        list2conjunction(List, Body),
        C = (body(OutputVarsFromPrevious,  Level, CHyp, OutFromHead) :- Body),
        assertz(for_the_top(C)).






/*
Builds a lists of LinkConditions.
LinkConditions are of the type
link(OneOfTheInputVariables, AvailableOutputVariables #fixed#, IndexOfTheInputVariable, IndexOfTheOutputVariables #to find through abfuction#, CurrentSet, Level)

The order of the input variables corresponds to the order they appear in the mode dec.
*/


%@  @item make_link_conditions(@var{+ListOfCurrentOutputs}, @var{+InputVariables}, @var{-LinkConditions}, @var{-Links})
%@  Given the set of current outputs (it's just a variable but it becomes an instantiated list during the learning)
%@  and a list of input variables, it creates a list of linkconditions that are conditions to be added to the rule (one for 
%@  each input variables and a list of Links, that is a list of variables (that become integer links during the learning). 
make_link_conditions([], _ListOfCurrentOutputs, [], [], []).


make_link_conditions([HT | Type], ListOfCurrentOutputs, [H | InputVariables], [LinkHere | LinkConditions], [IndexOut | OtherIndexes]) :-
        HT =.. [Ty | _],        
        LinkHere  =   link(Ty, H, ListOfCurrentOutputs, IndexOut),
                make_link_conditions(Type, ListOfCurrentOutputs, InputVariables, LinkConditions, OtherIndexes).                








%@ @item make_examples(Examples, MetaExamples)
%@ given a set of Examples, it produces literals of the type ex(A1HE, PosNeg) and assert clauses that need to be added to
%@ the top theory.


make_examples([], []).


make_examples([HE | TE], [ex(RealExample, PosNeg) | T1]) :-
        arg(1, HE, RealExample),
        arg(2, HE, PosNeg),
        (PosNeg > 0 ->
                (BodyList = 
                        [
                                increment_stat(times_selected(RealExample)),
                                RealExample
                        ]
                )
                ;
                (BodyList = 
                        [
                                increment_stat(times_selected(RealExample)),
                                \+(RealExample)
                        ]
                )
        ),
        list2conjunction(BodyList, Body),
        assertz(for_the_top((ex(RealExample, PosNeg) :- Body))),
        make_examples(TE, T1).
 




%@ @item %make_goal(MetaExamples)
%@ the goal is asserted

make_goal(MetaExamples) :-
        x_make_goal(MetaExamples, Goal),
        assertz(for_the_top(Goal)).        



x_make_goal(MetaExamples, ((goal :- Body))) :-
        list2conjunction(MetaExamples, Body).






   
make_statics :- 
        (
           bb_get_value(close_output, true) -> 
                LIT = finishlinks(Outputs, OutFromHead, OLL); 
                LIT = finishlinksnf(Outputs, OutFromHead, OLL)
        ),
%        assertz(for_the_top((                       %It cannot exist a partial rule that at a level L is different from another partial rule
%                                ic :-
%                                        pr(L, CS1, HA), 
%                                        pr(L, CS1, HB), 
%                                        HA =/= HB
%                        ))),
%        assertz(for_the_top((                       %We cannot have two different head output connections for the same rule
%                                ic :-
%                                        o(L, HA), 
%                                        o(L, HB), 
%                                        HA =/= HB
%                        ))),
       asserta(for_the_top((       
                                body(Outputs,  Level,[ B | C], OutFromHead) :- 
                                        pr(Level,  [B | C]),
                                        LIT,
                                        gpr(Level, [B | C]),                                       
                                        r(Level,  [B | C], OLL) 
                        ))),   
        assertz(for_the_top(abducible(pr(_, _)))),
        assertz(for_the_top(builtin(gpr(_, _)))),
        assertz(for_the_top(abducible(r(_, _, _)))),
        assertz(for_the_top(abducible(o(_, _)))),
        assertz(for_the_top(builtin(=<(_,_)))),
        assertz(for_the_top(builtin(<(_,_)))),
        assertz(for_the_top(builtin(is(_,_)))),
        assertz(for_the_top(builtin(increment_stat(_)))),
        assertz(for_the_top(builtin(check_vars(_)))),
        assertz(for_the_top(builtin(make_output_list(_, _, _)))),
        assertz(for_the_top(builtin(close_output(_,_,_)))),
        assertz(for_the_top(builtin(append(_,_,_)))),
        assertz(for_the_top(builtin(finishlinks(_, _,_)))),
        assertz(for_the_top(builtin(finishlinksnf(_, _,_)))),
        assertz(for_the_top(builtin(true))),
        assertz(for_the_top(builtin(verify(_)))),
        assertz(for_the_top(builtin(verify_order(_)))),
        assertz(for_the_top(builtin(link(_, _,_,_)))),
        assertz(for_the_top(builtin(nat(_)))),
        assertz(for_the_top(builtin(member(_,_)))).

        


%The following part is added to support integrity constraints for head mode declaration literals.

add_abducible_heads :-
        assertz(for_the_top(abducible(arwr(_)))).





%%%IC case

make_ic_for_ic([], _TOP, []).


make_ic_for_ic([(ic :- Body) | BT], M, [(ic :- BodyNew) | B2]) :- !,
        assert(originalic(((ic :- Body)))),                                                                    
        make_ic_for_ic_x(Body, M, BodyNew),
        make_ic_for_ic(BT, M, B2).     

        
make_ic_for_ic([A | BT], M, [A | B2]) :-
        make_ic_for_ic(BT, M, B2).



make_ic_for_ic_x((BH, Body), M, (BHN, BodyNew)) :- !,
        make_ic_for_ic_x(Body, M, BodyNew),
        make_ic_for_ic_xx(BH, M, BHN).
        
make_ic_for_ic_x(BH, M, BHN) :-        
        make_ic_for_ic_xx(BH, M, BHN).


make_ic_for_ic_xx(BH, M, arwr(BH)) :-
        tvar(BH,VBH),
        (member(modeh(VBH, _), M), ! ; member(modeh(VBH, _, _), M), !).

make_ic_for_ic_xx(BH, _Top, BH).